i, x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Type, f:(State(ds)Valtype(da;k)ds(x)?Void).
@i: with declarations 
ds:ds
da:da

effect of k(v) is x := f s v 
realizes es.
(x:Id. vartype(i;x)  ds(x)?Top)
& (e:E. loc(e) = i  Id  valtype(e)  Valtype(da;kind(e)))
& ((isrcv(k)  destination(lnk(k)) = i)  kindtype(i;k)  Valtype(da;k))
& (e:E.
& (loc(e) = i  Id  kind(e) = k  Knd  (x after e) = f((state when e),val(e))  ds(x)?Top) 

latex

Definitions	t  T, x. t(x), x:A. B(x), x(s), P  Q
Lemmas	es-after wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-val wf, es-valtype wf, ma-valtype wf